

Checking transition consistency


msc diagrams: three_way_connect(35) and CW_answer(24)
INCONSISTENCY:
Matching formula: k35 = k24
Precondition 1: rel (m35 , k35 , connected) & rel (k35 , n35 , three_wayhold); Precondition 2: rel (n24 , k24 , ringing) & rel (k24 , m24 , connected);
Post condition 1: rel (m35 , n35 , three_wayconnected k35); Post condition 2: rel (k24 , m24 , cw hold connect n24);

msc diagrams: three_way_connect(35) and CW_switch1(23)
INCONSISTENCY:
Matching formula: k35 = k23
Precondition 1: rel (m35 , k35 , connected) & rel (k35 , n35 , three_wayhold); Precondition 2: rel (k23 , m23 , cw hold connect n23);
Post condition 1: rel (m35 , n35 , three_wayconnected k35); Post condition 2: rel (k23 , n23 , cw hold connect m23);

msc diagrams: three_way_teardown2(27) and CW_teardown3(15)
INCONSISTENCY:
Matching formula: (n27 = n15) & (m27 = m15) & (k27 = k15)
Precondition 1: rel (m27 , n27 , three_wayconnected k27); Precondition 2: rel (k15 , n15 , cw hold connect m15);
Post condition 1: state (m27 , dial); Post condition 2: state (m15 , diale);

msc diagrams: three_way_teardown2(26) and CW_teardown3(14)
INCONSISTENCY:
Matching formula: n26 = n14
Precondition 1: rel (m26 , n26 , three_wayconnected k26); Precondition 2: rel (k14 , n14 , cw hold connect m14);
Post condition 1: state (n26 , dial); Post condition 2: state (n14 , diale);

msc diagrams: three_way_teardown3(25) and CW_switch1(23)
INCONSISTENCY:
Matching formula: m25 = k23
Precondition 1: state (n25 , three_wayhold m25) & state (m25 , dial); Precondition 2: rel (k23 , m23 , cw hold connect n23);
Post condition 1: rel (m25 , n25 , connected); Post condition 2: rel (k23 , n23 , cw hold connect m23);

msc diagrams: three_way_teardown3(25) and CW_switch2(22)
INCONSISTENCY:
Matching formula: m25 = k22
Precondition 1: state (n25 , three_wayhold m25) & state (m25 , dial); Precondition 2: rel (k22 , m22 , cw hold);
Post condition 1: rel (m25 , n25 , connected); Post condition 2: rel (k22 , m22 , connected);